(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_NRA)
(declare-fun v0 () Real)
(declare-fun v1 () Real)
(assert (let ((e2 2))
(let ((e3 0))
(let ((e4 7))
(let ((e5 (+ v1 v1)))
(let ((e6 (* v0 v0)))
(let ((e7 (- v1)))
(let ((e8 (/ e2 e4)))
(let ((e9 (+ e8 v1)))
(let ((e10 (* e5 e6)))
(let ((e11 (- e10)))
(let ((e12 (- e7)))
(let ((e13 (+ e7 e7)))
(let ((e14 (/ e4 e4)))
(let ((e15 (- v0 e14)))
(let ((e16 (+ v1 v0)))
(let ((e17 (+ e6 e9)))
(let ((e18 (+ e12 e12)))
(let ((e19 (/ e4 e2)))
(let ((e20 (/ e4 e4)))
(let ((e21 (- e9)))
(let ((e22 (/ e4 (- e2))))
(let ((e23 (- e7 e12)))
(let ((e24 (* (- e3) e22)))
(let ((e25 (<= e13 e21)))
(let ((e26 (distinct e15 e24)))
(let ((e27 (> e20 v0)))
(let ((e28 (< e24 e16)))
(let ((e29 (< e9 e18)))
(let ((e30 (distinct e5 e9)))
(let ((e31 (= e16 e18)))
(let ((e32 (= e14 e16)))
(let ((e33 (< e17 e7)))
(let ((e34 (= e24 e9)))
(let ((e35 (distinct e5 e8)))
(let ((e36 (distinct e13 e16)))
(let ((e37 (> e10 e20)))
(let ((e38 (<= e18 e9)))
(let ((e39 (< e5 e20)))
(let ((e40 (= e17 e19)))
(let ((e41 (< v0 e8)))
(let ((e42 (distinct e13 e9)))
(let ((e43 (< e11 e18)))
(let ((e44 (< e7 e24)))
(let ((e45 (< e24 e5)))
(let ((e46 (<= e5 e20)))
(let ((e47 (<= e11 e14)))
(let ((e48 (< e8 e18)))
(let ((e49 (<= e11 e9)))
(let ((e50 (= e11 e14)))
(let ((e51 (> e21 e24)))
(let ((e52 (< v1 e21)))
(let ((e53 (= e21 e22)))
(let ((e54 (distinct e9 v0)))
(let ((e55 (<= v0 e9)))
(let ((e56 (>= e9 e17)))
(let ((e57 (= e22 e16)))
(let ((e58 (= v0 e10)))
(let ((e59 (> e15 e6)))
(let ((e60 (> e15 e21)))
(let ((e61 (= e13 e11)))
(let ((e62 (distinct v0 e13)))
(let ((e63 (> e16 e16)))
(let ((e64 (<= e19 e23)))
(let ((e65 (= e6 v0)))
(let ((e66 (<= e15 e9)))
(let ((e67 (= e14 e10)))
(let ((e68 (> e11 e16)))
(let ((e69 (<= e23 v1)))
(let ((e70 (distinct v0 e8)))
(let ((e71 (<= v0 e14)))
(let ((e72 (= e6 e8)))
(let ((e73 (distinct e10 e8)))
(let ((e74 (< v1 e17)))
(let ((e75 (= e22 e20)))
(let ((e76 (> e12 v0)))
(let ((e77 (< e20 v0)))
(let ((e78 (> v1 e21)))
(let ((e79 (< e23 e16)))
(let ((e80 (distinct e19 e20)))
(let ((e81 (distinct e9 e7)))
(let ((e82 (> e14 e19)))
(let ((e83 (>= e11 e12)))
(let ((e84 (>= e11 e5)))
(let ((e85 (= e17 e24)))
(let ((e86 (<= e14 e21)))
(let ((e87 (< e8 e7)))
(let ((e88 (<= e11 e9)))
(let ((e89 (<= e9 e20)))
(let ((e90 (= e18 e18)))
(let ((e91 (< e13 e11)))
(let ((e92 (< e14 e11)))
(let ((e93 (< e24 e11)))
(let ((e94 (>= e10 e21)))
(let ((e95 (>= e15 e18)))
(let ((e96 (<= e13 e9)))
(let ((e97 (> e9 e8)))
(let ((e98 (> e11 e13)))
(let ((e99 (= e14 e11)))
(let ((e100 (<= v0 v1)))
(let ((e101 (< e17 e5)))
(let ((e102 (>= e23 e23)))
(let ((e103 (< v1 e18)))
(let ((e104 (= e16 e9)))
(let ((e105 (= v0 e13)))
(let ((e106 (>= v1 e14)))
(let ((e107 (<= e21 e23)))
(let ((e108 (>= v1 e6)))
(let ((e109 (<= v0 e18)))
(let ((e110 (>= e6 e6)))
(let ((e111 (< e15 e24)))
(let ((e112 (<= e14 e20)))
(let ((e113 (= e22 e19)))
(let ((e114 (xor e102 e100)))
(let ((e115 (or e81 e76)))
(let ((e116 (ite e101 e43 e53)))
(let ((e117 (and e69 e40)))
(let ((e118 (=> e41 e91)))
(let ((e119 (not e112)))
(let ((e120 (ite e84 e57 e86)))
(let ((e121 (not e108)))
(let ((e122 (or e65 e116)))
(let ((e123 (not e117)))
(let ((e124 (xor e80 e68)))
(let ((e125 (not e77)))
(let ((e126 (= e79 e39)))
(let ((e127 (or e63 e49)))
(let ((e128 (or e50 e78)))
(let ((e129 (and e83 e124)))
(let ((e130 (and e30 e32)))
(let ((e131 (or e126 e38)))
(let ((e132 (or e70 e109)))
(let ((e133 (and e52 e36)))
(let ((e134 (and e89 e111)))
(let ((e135 (xor e128 e56)))
(let ((e136 (ite e90 e129 e114)))
(let ((e137 (not e74)))
(let ((e138 (xor e121 e55)))
(let ((e139 (ite e45 e37 e122)))
(let ((e140 (=> e93 e34)))
(let ((e141 (=> e140 e92)))
(let ((e142 (or e134 e120)))
(let ((e143 (= e27 e115)))
(let ((e144 (not e59)))
(let ((e145 (xor e132 e67)))
(let ((e146 (= e33 e82)))
(let ((e147 (and e28 e35)))
(let ((e148 (= e44 e141)))
(let ((e149 (= e73 e46)))
(let ((e150 (ite e42 e58 e138)))
(let ((e151 (ite e139 e105 e145)))
(let ((e152 (=> e104 e146)))
(let ((e153 (=> e26 e147)))
(let ((e154 (=> e119 e130)))
(let ((e155 (ite e62 e137 e72)))
(let ((e156 (= e149 e131)))
(let ((e157 (or e47 e48)))
(let ((e158 (=> e88 e123)))
(let ((e159 (xor e118 e66)))
(let ((e160 (ite e154 e159 e152)))
(let ((e161 (and e94 e113)))
(let ((e162 (= e51 e135)))
(let ((e163 (ite e162 e157 e25)))
(let ((e164 (or e161 e64)))
(let ((e165 (or e127 e150)))
(let ((e166 (= e164 e95)))
(let ((e167 (=> e155 e103)))
(let ((e168 (not e125)))
(let ((e169 (and e166 e96)))
(let ((e170 (xor e87 e142)))
(let ((e171 (and e148 e160)))
(let ((e172 (ite e136 e31 e60)))
(let ((e173 (ite e168 e85 e61)))
(let ((e174 (=> e97 e98)))
(let ((e175 (or e173 e174)))
(let ((e176 (xor e158 e29)))
(let ((e177 (or e110 e171)))
(let ((e178 (or e176 e172)))
(let ((e179 (= e133 e75)))
(let ((e180 (ite e99 e153 e156)))
(let ((e181 (and e163 e167)))
(let ((e182 (or e151 e181)))
(let ((e183 (= e107 e169)))
(let ((e184 (= e170 e177)))
(let ((e185 (xor e144 e165)))
(let ((e186 (xor e178 e143)))
(let ((e187 (and e183 e184)))
(let ((e188 (not e179)))
(let ((e189 (ite e106 e188 e71)))
(let ((e190 (= e187 e180)))
(let ((e191 (= e186 e175)))
(let ((e192 (=> e191 e54)))
(let ((e193 (ite e190 e190 e190)))
(let ((e194 (xor e185 e189)))
(let ((e195 (=> e193 e182)))
(let ((e196 (=> e195 e192)))
(let ((e197 (=> e194 e194)))
(let ((e198 (not e197)))
(let ((e199 (= e198 e196)))
e199
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
